\documentclass[10pt, a4paper]{article}
\usepackage[paper=a4paper, left=1.5cm, right=1.5cm, bottom=1.5cm, top=3.5cm]{geometry}
\usepackage[latin1]{inputenc}
\usepackage[spanish]{babel}
\usepackage{aed2-symb,aed2-itef,aed2-tad}
\usepackage{caratula}
\usepackage{fancyhdr}
\usepackage{latexsym}
\usepackage{lastpage}
\usepackage{calc}

\titulo{Trabajo Pr\'actico de Especificaci\'on\\AED2-TEG}
\materia{Algoritmos y Estructura de Datos II}
\grupo{Grupo 4}
\integrante{Cossio Mercado, Christian Gustavo}{000/00}{cgcossio@gmail.com}
\integrante{Martinez Soler, Rodrigo Miguel}{000/00}{miguelmsoler@gmail.com}
\integrante{Niikado, Marina Andrea}{711/07}{mariniik@yahoo.com.ar}
\integrante{Palladino, Patricio}{218/10}{email@patriciopalladino.com}

\def\contentsname{\'Indice}

\begin{document} 

    \maketitle

    \tableofcontents

    \pagestyle{fancy}
    \lhead{Cossio Mercado, Martinez Soler, Niikado, Palladino}
    \rhead{AED2-TEG}

    \newpage
 
    \section{Renombres de tipos}
    
        \ \newline
        {\bf TAD} \tadNombre{Continente} {\bf es} nat\\
        {\bf TAD} \tadNombre{Casillero} {\bf es} nat\\
        {\bf TAD} \tadNombre{Jugador} {\bf es} nat\\
        {\bf TAD} \tadNombre{Misi\'on} {\bf es} continente\\
        {\bf TAD} \tadNombre{Movimiento} {\bf es} nat\\
        {\bf TAD} \tadNombre{Definici\'onJugadores} {\bf es} dicc(jugador, tupla(casillero, misi\'on)) 

    \section{TAD \tadNombre{Tablero}}

        \begin{tad}{\tadNombre{Tablero}}

        \tadGeneros{tablero}

        \tadExporta{tablero, generadores, observadores, continente, casilleros, entranFlechas?, flechasEntrantes}
	\tadUsa{\tadNombre{Bool, Nat}}
        \tadIgualdadObservacional
            {t}{t'}{tablero}
            { continentes($t$) $\igobs$ continentes($t'$) $\land$\\
                    ($\forall c$:continente)
			($c \in$ continentes($t$) $\implies$
			  (casillerosContinente($t, c$)$\igobs$casillerosContinente($t', c$) $\land$
			      ($\forall k$:casillero) ($k \in$ casillerosContinente($t, c$) $\implies$  
			      ($\forall m$:movimiento) \\
			      (saleFlecha?($t,k,m$) $\igobs$ saleFlecha?($t',k,m$) $\land$ \\
			      (saleFlecha?($t,k,m$) $\implies$ \\
			      flechaSaliente($t,k,m$) $\igobs$ flechaSaliente($t',k,m$))))
			)
            }

        \tadObservadores
        \tadAlinearFunciones{casillerosContinente}{tablero/tab,casillero/k,movimiento/mv}

        \tadOperacion{continentes}{tablero}{conj(continente)}{}
        \ 
        \tadOperacion{casillerosContinente}{tablero/t,continente/c}{conj(casillero)}{$c \in continentes(t)$}
	\
        %\tadOperacion{movimientos}{tablero/t}{conj(movimiento)}{}
	%\
        \tadOperacion{saleFlecha?}{tablero/tab,casillero/k,movimiento/mv}{bool}{$k \in casilleros(tab)$}
        \ 
        \tadOperacion{flechaSaliente}{tablero/tab,casillero/k,movimiento/mv}{casillero}{$k \in casilleros(tab) \land saleFlecha?(tab, k, mv)$}

        \tadGeneradores
        \tadAlinearFunciones{AgregarFlechaDoble}{tablero/t,continente/c,casillero/nue,movimiento/ida}

        \tadOperacion{CrearTablero}{casillero,continente}{tablero}{}
        \ 
        \tadOperacion{AgregarCasillero}
            {tablero/tab,continente/cont,casillero/nue,movimiento/ida,casillero/vie,movimiento/vue}{tablero}
            {$nue \notin$ casilleros($tab$) $\land$ $vie \in$ casilleros($tab$) $\land$ $\neg$saleFlecha?(tab, vie, vue) $\land$ \\
	    ($cont$ = continente($tab, vie$) $\lor$ $cont \notin$ continentes($tab$))}
        \ 
        \tadOperacion{AgregarFlecha}
            {tablero/tab,casillero/ori,casillero/des,movimiento/mv}{tablero}
            {$ori \in$ casilleros($tab$) $\land$ $des$ $\in$ casilleros($tab$) $\land$ $\neg$saleFlecha?($tab,ori,mv$) $\land$ ($\exists m$:movimiento)(flechaSaliente($tab,des,m$) $\igobs$ ori)}
        \ 
        \tadOperacion{AgregarFlechaDoble}
            {tablero/tab,casillero/ori,movimiento/ida,casillero/des,movimiento/vue}{tablero}
	    {$ori \in$ casilleros($tab$) $\land$ $des$ $\in$ casilleros($tab$) $\land$ $\neg$saleFlecha?($tab,ori,ida$) $\land$ $\neg$saleFlecha?($tab,des,vue$)}


        \tadOtrasOperaciones
        \tadAlinearFunciones{entranFlechas?}{tablero/tab,casillero/k,movimiento/mv}

        \tadOperacion{continente}{tablero/tab,casillero/k}{continente}{$k \in$ casilleros($tab$)}
        \ 
        \tadOperacion{casilleros}{tablero}{conj(casillero)}{}
        \ 
        %\tadOperacion{flechas}{tablero}{dicc(tupla(casillero, movimiento), casillero)}{} %VER SI SE PUEDE SACAR
        %\ 
        \tadOperacion{entranFlechas?}{tablero/tab,casillero/k,movimiento/mv}{bool}{$k \in$ casilleros($tab$)}
        \ 
        \tadOperacion{flechasEntrantes}{tablero/tab,casillero/k,movimiento/mv}{conjunto(casillero)}{$k \in$ casilleros($tab$) $\land$ entranFlechas?($tab, k, mv$)}

        \tadAxiomas[\paratodo{casillero}{k, q,ori,des}, \paratodo{continente}{c, c'}, \paratodo{movimiento}{m,ida,vue}, \paratodo{tablero}{t}]
        \tadAlinearAxiomas{flechasEntrantes(AgregarFlechaDoble($t,ori,ida,des,vue$), $q, m$)}
	\
        \tadAxioma{continentes(CrearTablero($k,c$))}{Ag($c, \emptyset)$}
        \tadAxioma{continentes(AgregarCasillero($t,c,ori,ida,des,vue$))}{Ag($c,$ continentes($t$))}
        \tadAxioma{continentes(AgregarFlecha($t,ori,des,m$))}{continentes($t$)}
        \tadAxioma{continentes(AgregarFlechaDoble($t,ori,ida,des,vue$))}{continentes($t$)}
        \
        \tadAxioma{casillerosContinente(CrearTablero($k,c$), $c'$)}{Ag($k, \emptyset$)}
        \tadAxioma{casillerosContinente(AgregarCasillero($t,c,ori,ida,des,vue$), $c'$)}
            {
                \IF $c = c'$ THEN Ag($ori, \emptyset$) \\
                ELSE $\emptyset$ \\
                FI $\cup$ casillerosContinente($t, c'$)
            }
        \tadAxioma{casillerosContinente(AgregarFlecha($t,ori,des,m$), $c$)}{casillerosContinente($t,c$)}
        \tadAxioma{casillerosContinente(AgregarFlechaDoble($t,ori,ida,des,vue$), $c$)}{casillerosContinente($t,c$)}
        \ 
        \tadAxioma{saleFlecha?(CrearTablero($k,c$), $q$, $m$)}{false}
        \tadAxioma{saleFlecha?(AgregarCasillero($t,c,ori,ida,des,vue$), $q, m$)}
	    {(($ori=q\ \land\ m=ida$) $\lor$ ($des=q\ \land\ m=vue$)) $\lor$ saleFlecha?($t, q, m$)}
        \tadAxioma{saleFlecha?(AgregarFlecha($t,ori,des,m$), $q, m'$)}
	    {($ori = q\ \land\ m = m'$) $\lor$ saleFlecha?($t, q, m'$)}
        \tadAxioma{saleFlecha?(AgregarFlechaDoble($t,ori,ida,des,vue$), $q, m$)}
	    {(($ori=q\ \land\ m=ida$) $\lor$ ($des=q\ \land\ m=vue$)) $\lor$ saleFlecha?($t, q, m$)}
	\
        \tadAxioma{flechaSaliente(AgregarCasillero($t,c,ori,ida,des,vue$), $q, m$)}
            {\IF $ori=q\ \land\ ida=m$ THEN Ag($des, \emptyset$)
	      ELSE{ \IF $des=q\ \land\ m=vue$ THEN Ag($ori, \emptyset$)
		    ELSE flechaSaliente($t, q, m$)
		    FI
	      } 
	      FI
	    }
        \tadAxioma{flechaSaliente(AgregarFlecha($t,ori,des,m$), $q, m'$)}
	    {\IF $ori = q\ \land\ m = m'$ THEN $des$
	      ELSE flechaSaliente($t, q, m'$)
	      FI
	    }
        \tadAxioma{flechaSaliente(AgregarFlechaDoble($t,ori,ida,des,vue$), $q, m$)}
	    {\IF $ori=q\ \land\ ida=m$ THEN $des$
	      ELSE{ \IF $des=q\ \land\ m=vue$ THEN $ori$
		    ELSE flechaSaliente($t, q, m$)
		    FI
	      }
	      FI
	    }
	\
        \tadAxioma{continente(CrearTablero($k,c$), $q$)}{$c$}
        \tadAxioma{continente(AgregarCasillero($t,c,ori,ida,des,vue$), $q$)}
            {\IF $ori = q$ THEN $c$
                ELSE continente($t, q$)
                FI
            }
        \tadAxioma{continente(AgregarFlecha($t,ori,des,m$), $q$)}{continente($t, q$)}
        \tadAxioma{continente(AgregarFlechaDoble($t,ori,ida,des,vue$), $q$)}{continente($t, q$)}
	\
        \tadAxioma{casilleros(CrearTablero($k,c$))}{Ag($k, \emptyset$)}
        \tadAxioma{casilleros(AgregarCasillero($t,c,ori,ida,des,vue$))}{Ag($ori,$ casilleros($t$))}
        \tadAxioma{casilleros(AgregarFlecha($t,ori,des,m$))}{casilleros($t$)}
        \tadAxioma{casilleros(AgregarFlechaDoble($t,ori,ida,des,vue$))}{casilleros($t$)}
        \ 
        \tadAxioma{entranFlechas?(CrearTablero($k,c$)$, q, m$)}{false}
        \tadAxioma{entranFlechas?(AgregarCasillero($t,c,ori,ida,des,vue$), $q, m$)}
            {(($ori=q\ \land\ m=vue$) $\lor$ ($des=q\ \land\ m=ida$)) $\lor$ entranFlechas?($t, q, m$)}
        \tadAxioma{entranFlechas?(AgregarFlecha($t,ori,des,m$), $q,m'$)}
            {($des = q\ \land\ m = m'$) $\lor$ entranFlechas?($t, q, m'$)}
        \tadAxioma{entranFlechas?(AgregarFlechaDoble($t,ori,ida,des,vue$), $q, m$)}
	    {(($ori=q \land m=vue$)$\lor$($des=q \land m=ida$)) $\lor$ entranFlechas?($t, q, m$)}
        \ 
        \tadAxioma{flechasEntrantes(AgregarCasillero($t,c,ori,ida,des,vue$), $q, m$)}
            {\IF $ori=q\ \land\ m=vue$ THEN Ag($des, \emptyset$)
	      ELSE{ \IF $des=q\ \land\ m=ida$ THEN Ag($ori, \emptyset$)
		    ELSE $\emptyset$
		    FI
	      } $\cup$ flechasEntrantes($t, q, m$)
	      FI
	    }
        \tadAxioma{flechasEntrantes(AgregarFlecha($t,ori,des,m$), $q, m'$)}
	    {\IF $des = q\ \land\ m = m'$ THEN Ag($ori, \emptyset$)
	      ELSE $\emptyset$
	      FI $\cup$ flechasEntrantes($t, q, m'$)	  
	    }
        \tadAxioma{flechasEntrantes(AgregarFlechaDoble($t,ori,ida,des,vue$), $q, m$)}
	    {\IF $ori=q\ \land\ vue=m$ THEN Ag($des, \emptyset$)
	      ELSE{ \IF $des=q\ \land\ m=ida$ THEN Ag($ori, \emptyset$)
		    ELSE $\emptyset$
		    FI
	      }
	      FI $\cup$ flechasEntrantes($t, q, m$)
	    }

        \end{tad}
      
\newpage
	\section{TAD \tadNombre{Juego}}

        \begin{tad}{\tadNombre{Juego}}

        \tadGeneros{juego}

        \tadExporta{juego, generadores, observadores, eliminado?, terminado?, ganador, casillerosAMisi\'on?,\\jugadoresCasillero, casilleroDisputado?, casilleroDominado?, casilleroVac\'io?}
	\tadUsa{\tadNombre{Tablero, Bool, Nat}}
        \tadIgualdadObservacional
            {j}{j'}{juego}
            { tablero($j$) $\igobs$ tablero($j'$) $\land$ jugadores($j$) $\igobs$ jugadores($j'$) $\land$
                ($\forall jug$ : jugador)\\($jug$ $\in$ jugadores($j$) $\implies$ (misi\'on($j, jug$) $\igobs$ misi\'on($j',jug$) $\land$ fichasAgregadas($j, jug$) $\igobs$ fichasAgregadas($j', jug$) $\land$\\
		($\forall k$ : casillero)($k$ $\in$ casilleros(tablero($j$)) $\implies$ 
                    fichas($j, jug, k$) $\igobs$ fichas($j', jug, k$))
	    }

        \tadObservadores
        \tadAlinearFunciones{fichasAgregadas}{juego/j, jugador/jug, casillero/k}

        \tadOperacion{tablero}{juego}{tablero}{}
	\
        \tadOperacion{jugadores}{juego}{conj(jugador)}{}
	\
        \tadOperacion{fichas}{juego/j, jugador/jug, casillero/k}{nat}{$jug \in$ jugadores($j$) $\land$ $k \in$ casilleros(tablero($j$))}
	\
	\tadOperacion{fichasAgregadas}{juego/j, jugador/jug}{nat)}{$jug \in$ jugadores($j$)}
	\
	\tadOperacion{misi\'on}{juego/j, jugador/jug}{misi\'on)}{$jug \in$ jugadores($j$)}

        \tadGeneradores
	\tadAlinearFunciones{AgregarJugador}{juego/j, jugador/jug, casillero/k, mision/ms}		  
	\
	\tadOperacion{CrearJuego}{tablero/t, definici\'onJugadores/djugs}{juego}
	    {$\lnot\emptyset?$(claves($djugs$)) $\land$ ($\forall jug$:jugador)(def?($jug, djugs$) $\implies$  
	     (casilleroInicial($djugs, jug$) $\in$ casilleros($t$) $\land$ misi\'on($djugs, jug$) $\in$ continentes(t) $\land$ ($\forall jug'$:jugador)(def?($jug',djugs$) $\implies$\\ ($jug \igobs jug'$ $\Leftrightarrow$ casilleroInicial($djugs, jug$) $\igobs$ casilleroInicial($djugs, jug'$)))))}
	\
	%\tadOperacion{AgregarJugador}{juego/j, jugador/jug, casillero/k, misi\'on/ms}{juego}
        %    {$\lnot$iniciado($j$) $\land$ $jug \notin$ jugadores($j$) $\land$ $k \in$ casilleros(tablero($j$)) $\land$ casilleroVac\'io?(k) $\land$ $ms \in$ continentes(tablero($j$)) }
	%\
        \tadOperacion{AgregarFicha}{juego/j, jugador/jug, casillero/k}{juego}
            {$\lnot$terminado?($j$) $\land$ $jug \in$ jugadores($j$) $\land$ $\lnot$eliminado?($j, jug$) $\land$ $k \in$ casilleros(tablero($j$)) $\land$ (casilleroVacio?($j, k$) $\lor$ (casilleroDominado?($j, k$) $\land$ dominante($j, k$) $\igobs jug$))}
	\        
	\tadOperacion{Mover}{juego/j, jugador/jug, movimiento/k, nat/cant}{juego}
            {$\lnot$terminado?($j$) $\land$ $jug \in$ jugadores($j$) $\land$ $\lnot$eliminado?($j, jug$)}

        \tadOtrasOperaciones
        \tadAlinearFunciones{generarMulticonjCasillero}{juego/j, jugador/jugm, movimiento/mv }
        %\tadOperacion{iniciado?}{juego/j}{bool}{}
	\tadOperacion{terminado?}{juego/j}{bool}{}
	\tadOperacion{eliminado?}{juego/j, jugador/jug}{bool}{$jug \in$ jugadores($j$)}
	%\tadOperacion{esGanador?}{juego/j, jugador/jug}{bool} {$jug \in$ jugadores($j$)}
	\tadOperacion{cumpli\'oMisi\'on?}{juego/j, jugador/jug}{bool}{$jug \in$ jugadores($j$)}
	\tadOperacion{algunoCumpli\'Misi\'on?}{juego/j, conj(jugador)/jugs}{bool}{$jugs \subseteq$ jugadores($j$)}
	\tadOperacion{casilleroVacio?}{juego/j, casillero/k}{bool}{$k \in$ casilleros(tablero($j$))}
	\tadOperacion{casilleroDominado?}{juego/j, casillero/k}{bool}{$k \in$ casilleros(tablero($j$))}
	\tadOperacion{casilleroDisputado?}{juego/j, casillero/k}{bool}{$k \in$ casilleros(tablero($j$))}
	\tadOperacion{casillerosNoDominados}{juego/j, jugador/jug, conj(casillero)/ks, jugador/jugm, movimiento/mv, nat/cant}{nat}{$jug \in$ jugadores($j$) $\land$ $jugm$ $\in$ jugadores($j$) $\land$ $ks$ $\subseteq$ casilleros(tablero($j$))}
	\tadOperacion{perdedorBatalla}{juego/j, casillero/k}{jugador}{$k \in$ casilleros(tablero($j$)) $\land$ casilleroDisputado?($j,k$)}
        \tadOperacion{jugadoresCasillero}{juego/j, casillero/k}{conj(jugador)}{$k \in$ casilleros(tablero($j$))}
	\tadOperacion{jugadoresCasilleros}{juego/j, conj(casillero)/ks}{conj(jugador)}{$ks \subseteq$ casilleros(tablero($j$))}
        \tadOperacion{misi\'on}{definici\'onJugadores/djugs, jugador/jug}{misi\'on)}{$jug \in$ claves($djugs$)}
	\tadOperacion{casillerosMisi\'on}{juego/j, jugador/jug}{conj(casillero)}{$jug$ $\in$ jugadores($j$))}
	\tadOperacion{casillerosAMisi\'on}{juego/j, jugador/jug}{nat}{$jug \in$ jugadores($j$)}
	\tadOperacion{calcIngresos}{juego/j, jugador/jug, conj(casillero)/ks, nat/cant}{nat}{$jug \in$ jugadores($j$) $\land$ $ks \subseteq$ casilleros(tablero($j$))}
	\tadOperacion{calcEgresos}{juego/j,jugador/jug,movimiento/mv,nat/cant,casillero/k}{nat}{$jug$ $\in$ jugadores($j$) $\land$ k $\in$ casilleros(tablero($j$))}
	\tadOperacion{fichasCasillero}{juego/j, jugador/jug, movimiento/mv, nat/cant, casillero/k}{nat}{$jug \in$ jugadores($j$) $\land$ $k \in$ casilleros(tablero($j$))}
	\tadOperacion{fichasJugador}{juego/j, jugador/jugm, movimiento/mv, nat/cant, casillero/k, jugador/jug}{nat}{$jug \in$ jugadores($j$) $\land$ $jugm \in$ jugadores($j$) $\land$ $k \in$ casilleros(tablero($j$))}
	\tadOperacion{fichasJugador}{juego/j,jugador/jug,conj(casillero)/ks}{nat}{$jug$ $\in$ jugadores($j$) $\land$ $ks$ $\subseteq$ casilleros(tablero($j$))}
	\tadOperacion{fichasJugadores}{juego/j,conj(jugador)/jugs,casillero/k}{nat}{$jugs$ $\subseteq$ jugadores($j$) $\land$ $k$ $\in$ casilleros(tablero($j$))}
	\tadOperacion{obtenerGanador}{juego/j, conj(jugador)/jugs}{jugador}{terminado?($j$) $\land jugs \subseteq$ jugadores($j$) }
	\tadOperacion{ganador}{juego/j}{jugador}{terminado?($j$)}
	\tadOperacion{dominante}{juego/j, casillero/k}{jugador}{$k \in$ casilleros(tablero($j$)) $\land$ casilleroDominado?($jue,k$)}
	\tadOperacion{definici\'onJugador}{juego/j, jugador/jug}{tupla(casillero,misi\'on)}{$jug \in$ jugadores($j$)}
	\tadOperacion{casilleroInicial?}{juego/j, casillero/k}{bool}{$k \in$ casilleros(tablero($j$))}
	\tadOperacion{casilleroInicial?}{conj(jugador)/jugs, definici\'onJugadores/djugs, casillero/k}{bool}{}
	\tadOperacion{casilleroInicial}{juego/j, jugador/jug}{casillero}{$jug \in$ jugadores($j$)}
	\tadOperacion{casilleroInicial}{definici\'onJugadores/djugs, jugador/jug}{casillero}{$jug \in$ claves($djugs$)}
	\tadOperacion{jugadorAlInicio}{definici\'onJugadores/djugs,casillero/k}{jugador}{casilleroInicial?($djugs, k$)}
	\tadOperacion{jugadorAlInicio}{conj(jugador)/jugs, definici\'onJugadores/djugs,casillero/k}{jugador}{casilleroInicial?($djugs, k$)}  
	\tadOperacion{casilleroMulticonj}{juego/j,casillero/k}{multiconj(jugador)}{$k$ $\in$ casilleros(tablero(j))}
	\tadOperacion{generarMulticonjCasillero}{juego/j,conj(jugador)/jugs,casillero/k}{multiconj(jugador)}{$jugs$ $\subseteq$ jugadores($j$) $\land$ $k$ $\in$ casilleros(tablero($j$))}
	\tadOperacion{agregarMultJugs}{jugador/jug,nat/cant}{multiconj(jugador)}{}

	\tadAxiomas[\paratodo{juego}{j}, \paratodo{casillero}{k,k'}, \paratodo{nat}{cant}, \paratodo{movimiento}{mv}, \paratodo{tablero}{tab}, \paratodo{jugador}{jug, jug', jugm}, \paratodo{misi\'on}{mis}, \paratodo{definici\'onJugadores}{djugs}]
        \tadAlinearAxiomas{jugadoresCasillero(AgregarJugador($j, jug, k, ms$)$, k'$)}

        \tadAxioma{tablero(CrearJuego($tab,djugs$))}{$tab$}
        \tadAxioma{tablero(AgregarFicha($j, jug, k$))}{tablero($j$)}
	\tadAxioma{tablero(Mover($j, jug, mv, cant$))}{tablero($j$)}
	\
        \tadAxioma{jugadores(CrearJuego($tab,djugs$))}{claves($djugs$)}
        \tadAxioma{jugadores(AgregarFicha($j, jug, k$))}{jugadores($j$)}
	\tadAxioma{jugadores(Mover($j, jug, mv, cant$))}{jugadores($j$)}
	\
        \tadAxioma{fichas(CrearJuego($tab,djugs$), $jug, k$)}{ \IF casilleroInicial($djugs,jug$)=$k$ THEN 1 ELSE 0 FI}
        %\tadAxioma{fichas(AgregarJugador($j, jug, k, ms$)$, jug', k'$)}{ \IF $jug=jug'$ THEN{ \IF $k=k'$ THEN 1 ELSE 0 FI}
	%								     ELSE fichas($j, jug', k'$) FI }
        \tadAxioma{fichas(AgregarFicha($j, jug, k$)$, jug', k'$)}{ \IF $k=k' \land jug=jug'$ THEN 1 ELSE 0 FI \\+ fichas($j, jug', k'$)}
	\tadAxioma{fichas(Mover($j, jug, mv, cant$)$, jug', k$)}{fichasJugador($j, jug, mv, cant, k, jug'$)}
	\
	%\tadAxioma{fichasTotales(AgregarJugador($j, jug, k, ms$), $jug'$)}{\IF $jug=jug'$ THEN 1 ELSE fichasTotales($j, jug'$) FI}
	\tadAxioma{fichasAgregadas(CrearJuego($tab,djugs$), $jug$)}{1}
	\tadAxioma{fichasAgregadas(AgregarFicha($j, jug, k$)$, jug'$)}{\IF $jug=jug'$ THEN 1 ELSE 0 FI \\+ fichasAgregadas(j, jug')}
	\tadAxioma{fichasAgregadas(Mover($j, jug, mv, cant$)$, jug'$)}{fichasAgregadas($j, jug'$)}
	\
	%\tadAxioma{misi\'on(AgregarJugador($j, jug, k, ms$)$, jug'$)}{\IF $jug=jug'$ THEN $ms$ ELSE misi\'on($j, jug'$) FI}
	%\tadAxioma{misi\'on(AgregarFicha($j, jug, k$)$, jug'$)}{misi\'on($j, jug'$)}
	\tadAxioma{misi\'on($j, jug$)}{$\Pi_2$(definici\'onJugador($j,jug$))}
	\tadAxioma{misi\'on($djugs, jug$)}{$\Pi_2$(obtener($jug,djugs$))}
	\
	\tadAxioma{casilleroInicial?($djugs, k$)}{casilleroInicial?(claves($djugs$), $djugs, k$)}	  
	\tadAxioma{casilleroInicial?($jugs, djugs, k$)}{$\lnot\emptyset$?($jugs$) $\land$ (casilleroInicial($djugs$,dameUno($jugs$))=$k$ $\lor$ casilleroInicial?(sinUno($jugs$),$djugs, k$))}
	\
	\tadAxioma{casilleroInicial($j, jug$)}		{$\Pi_1$(definici\'onJugador($j,jug$))}
	\tadAxioma{casilleroInicial($djugs, jug$)}	{$\Pi_1$(obtener($jug,djugs$))}
	\
	\tadAxioma{fichasJugadores($j, jugs, k$)}{\IF $\emptyset$?($jugs$) THEN 0 ELSE fichas($j, $dameUno($jugs$)$, k$) + fichasJugadores($j, $sinUno($jugs$)$, k$) FI}
	\
	\tadAxioma{fichasJugador($j, jug, ks$)}{\IF $\emptyset$?($ks$) THEN 0 ELSE fichas($j, jug, $dameUno($ks$)) + fichasJugador($j, jug, $sinUno($ks$)) FI}
	\
	\tadAxioma{fichasJugador($j, jugm, mv, cant, k, jug$)}{\IF $jugm=jug$ 
								      THEN{ fichas($j, jug, k$)\\
									  %- \IF saleFlecha?($j, k, mv$) $\land$ casilleroDominado($j, k$) $\land$ dominante($j, k$) $= jug'$
									  %  THEN min(fichas($j, jug', k$)$, cant$) ELSE 0 FI
									  $-$ calcEgresos($j, jug, mv, cant, k$)\\
									  + calcIngresos($j, jug', $flechasEntrantes($j, k, mv$)$, cant$) }
								      ELSE fichas($j, jug, k$) FI\\
								      $-$ \IF casilleroDisputado?($j, k$) $\land$ \\$jug=$ perdedorBatalla($j, k$) THEN 1 ELSE 0 FI
								    }

	\
	\tadAxioma{jugadoresCasillero(CrearJuego($tab,djugs$)$, k$)}{\IF casilleroInicial?($djugs, k$) THEN jugadorAlInicio($djugs, k$) ELSE $\emptyset$ FI}
	\tadAxioma{jugadoresCasillero(AgregarFicha($j, jug, k$)$, k'$)}{\IF $k=k'$ THEN Ag($jug, \emptyset$) ELSE jugadoresCasillero($j, k'$) FI}
	\tadAxioma{jugadoresCasillero(Mover($j, jug, mv, cant$)$, k$)}{\IF fichasJugador($j, jug, mv, cant, k, jug$) $>$ 0
									     THEN Ag($jug, $jugadoresCasillero($j, k$)) ELSE jugadoresCasillero($j, k$) $-$ \{$jug$\} FI}
	\
	\tadAxioma{jugadoresCasilleros($j, ks$)}{\IF $\emptyset$?($ks$) THEN $\emptyset$ 
							ELSE jugadoresCasillero($j, $dameUno($ks$)) $\cup$ jugadoresCasilleros($j, $sinUno($ks$)) FI}
	\
	\tadAxioma{casilleroVac\'io?($j, k$)}{\#(jugadoresCasillero($j, k$)) $=$ 0}
	\
	\tadAxioma{casilleroDominado?($j, k$)}{\#(jugadoresCasillero($j, k$)) $=$ 1}
	\tadAxioma{casilleroDisputado?($j, k$)}{\#(jugadoresCasillero($j, k$)) $>$ 1}
	\
	\tadAxioma{casillerosMisi\'on($j, jug$)}{casillerosContinente(tablero($j$),  misi\'on($j, jug$))}
	%\tadAxioma{casillerosMisi\'on($tab, jug$)}{casillerosContinente($tab$,  misi\'on($j, jug$))}
	\
	\tadAxioma{casillerosAMisi\'on(CrearJuego($tab,djugs$), $jug$)}{\#(casillerosContinente($tab$, misi\'on($djugs,jug$)))$-$ \IF casilleroInicial($djugs,jug$) $\in$ casillerosContinente($tab$,misi\'on($djugs,jug$)) THEN 1 ELSE 0 FI }
	\tadAxioma{casillerosAMisi\'on(AgregarFicha($j, jug, k$)$, jug'$)}{casillerosAMisi\'on($j, jug'$) $-$\\
									  \IF casilleroVac\'io?($j, k$) THEN 1 ELSE 0 FI}
	\tadAxioma{casillerosAMisi\'on(Mover($j, jug, mv, cant$)$, jug'$)}{casillerosNoDominados($j, jug'$,\\casillerosMisi\'on($j,jug'$), $jug, mv, cant$)}
	\
	\tadAxioma{cumpli\'oMisi\'on?($j, jug$)}{casillerosAMisi\'on($j, jug$) $=$ 0}
	\tadAxioma{algunoCumpli\'oMisi\'on?($j, jugs$)}{\IF $\emptyset$?($jugs$) THEN false ELSE cumpli\'oMisi\'on($j, $dameUno($jugs$)) $\lor$ algunoCumpli\'oMisi\'on?($j, $sinUno($jugs$)) FI}
	\
	\tadAxioma{calcIngresos($j, jug, ks, cant$)}{\IF $\emptyset$?($ks$) THEN 0 
							  ELSE {\IF casilleroDominado?($j$,dameUno($ks$)) $\land$  dominante($j, $dameUno($ks$))$=jug$ 
								THEN  min(fichas($j, jug, $dameUno($ks$))$, cant$) ELSE 0
								FI + calcIngresos($j, jug, $sinUno($ks$)$, cant$)}
							  FI }
	\
	\tadAxioma{calcEgresos($j, jug, mv, cant, k$)}{\IF saleFlecha?(tablero($j$), $k, mv$) $\land$ casilleroDominado?($j, k$) $\land$ dominante($j, k$) = $jug$ 
								  THEN min(fichas($j, jug, k$)$, cant$) ELSE 0 FI
							    }
	\
	\tadAxioma{fichasCasillero($j, jug, mv, cant, k$)}{fichasJugadores($j$, jugadoresCasillero($k$), $k$)\\
								$-$  calcEgresos($j, jug, mv, cant, k$)\\
								+ calcIngresos($j, jug, $flechasEntrantes($j, k, mv$)$, cant$)\\
								$-$ \IF casilleroDisputado?($j, k$) THEN 1 ELSE 0 FI 
								}
	\
	\tadAxioma{casillerosNoDominados($j, jug, ks, jugm, mv, cant$)}{\IF $\emptyset$?($ks$) THEN 0
									ELSE{
									\IF fichasJugador($j, jugm, mv, cant, $\\dameUno($ks$)$, jug$) = fichasCasillero($j, jugm, mv, cant, $dameUno($ks$)) THEN  0 ELSE 1
									FI\\
									+ casillerosNoDominados($j, jug, $\\sinUno($ks$)$, jugm, mv, cant$)}
									FI  }
	%\tadAlinearAxiomas{obtenerGanador($j, jugs$)}
	\
	\tadAxioma{dominante($j, k$)}{dameUno(jugadoresCasillero($j, k$))}
	\
	\tadAxioma{eliminado?($j, jug$)}{fichasJugador($j, jug, $casilleros(tablero($j$))) = 0}
	\
	\tadAxioma{terminado?($j$)}{\#(jugadoresCasilleros($j, $casilleros(tablero($j$)))) = 1 $\lor$ \\ algunoCumpli\'oMisi\'on?($j, $jugadores($j$))}
	\
	\tadAxioma{obtenerGanador($j, jugs$)}{\IF cumpli\'oMisi\'on?($j, $dameUno($jugs$)) $\lor$ \\ (\#(jugadoresCasilleros($j, $casilleros(tablero($j$)))) = 1  $\land$ \\ dameUno($jugs$)  $\in$  jugadoresCasilleros($j, $casilleros(tablero($j$)))
						THEN dameUno($jugs$) ELSE obtenerGanador($j, $sinUno($jugs$) FI }
	\
	\tadAxioma{ganador($j$)}{obtenerGanador($j, $jugadores($j$))}
	\
	\tadAxioma{definici\'onJugador(CrearJuego($tab, djugs$),$jug$)}{obtener($jug, djugs$)}
	\tadAxioma{definici\'onJugador(AgregarFicha($j, jug, k$)$, jug'$)}{definici\'onJugador($j,jug'$)}
	\tadAxioma{definici\'onJugador(Mover($j, jug, mv, cant$)$, jug'$)}{definici\'onJugador($j,jug'$)}	  
	\
	\tadAxioma{jugadorAlInicio($djugs, k$)}{jugadorAlInicio(claves($djugs$), $djugs, k$)}	  
	\tadAxioma{jugadorAlInicio($jugs, djugs, k$)}{\IF jugadorAlInicio($djugs$,dameUno($jugs$))=$k$ THEN dameUno($jugs$) ELSE jugadorAlInicio(sinUno($jugs$),$djugs, k$) FI}
	\
	\tadAlinearAxiomas{generarMulticonjCasillero($j, jugs, k$)}
	\tadAxioma{perdedorBatalla($j, k$)}{dameUno(casilleroMulticonj($j,k$))}
	\
	\tadAxioma{casilleroMulticonj($j,k$)}{generarMulticonjCasillero($j$,jugadoresCasillero($j,k$),$k$)}
	\
	\tadAxioma{generarMulticonjCasillero($j, jugs, k$)}{\IF $\emptyset$?($jugs$) THEN $\emptyset$ ELSE agregarMultJugs(dameUno($jugs$), fichas($j$,dameUno($jugs$),$k$)) $\cup$ generarMulticonj($j, sinUno(jugs), k$)  FI}
	\
	\tadAxioma{agregarMultJugs($jug, cant$)}{\IF $cant$=0 THEN $\emptyset$ ELSE Ag($jug$, agregarMultJugs($jug$,pred($cant$))) FI}

        \end{tad}

\end{document}
